L:(es_realizer{i:l} List). 
pairwise(A,B.R-compat{i:l}(A; B); L)
 l_all(L; es_realizer{i:l}; A.R-Feasible{i:l}(A))
 R-Feasible{i:l}
 R-Feasible(Rlist(L)) 

latex

Definitions	tt, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , R-compat{i:l}(A; B), x,y. t(x;y), x. t(x), P  Q, False, A, A  B, prop{i:l}, Y, reduce(f; k; as), True, ||as||, Rlist(L), R-Feasible{i:l}(R), l_all(L; T; x.P(x)), pairwise(x,y.P(x;y); L), P  Q, t  T, x:A. B(x), x(s1,s2), x(s), P  Q, lelt(i; j; k), int_seg(i; j)
Lemmas	R-compat-none, Rlist wf, R-compat-symmetry, pairwise wf, l all wf2, pairwise-cons, l all cons, length wf2, select wf, R-compat wf, int seg wf, R-Feasible wf, l member wf, es realizer wf